A:Type, B:(AType), f:fpf(A; a.B(a)), eq:EqDecider(A), x:A, z:B(x).
fpf-cap(f; eq; x; z)  B(x) 

latex

Definitions	x:A. B(x), x(s), t  T, fpf-cap(f; eq; x; z), if b then t else f fi , x. t(x), P  Q, tt, ff, prop{i:l}, , Unit, P  Q, P  Q,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, deq wf, fpf wf